p:FinProbSpace, f:(), X:(n:RandomVariable(p;f(n))).
(X(n) as n)  (Outcome) 

latex

Definitions	t  T, x:A. B(x), Outcome, x:AB(x), S  T, x(s), P  Q, False, A, P & Q, A  B, i  j < k, , {x:A| B(x)} , , {i..j}, f(a), RandomVariable(p;n), , Type, #$n, suptype(S; T), r  s, , x:A  B(x), x:A. B(x), x.A(x), (X(n) as n), FinProbSpace
Lemmas	random-variable wf, finite-prob-space wf, rationals wf, qle wf, le wf, int seg wf, nat wf, p-outcome wf